$\forall$$k$:Knd, ${\it da}$, ${\it da'}$:$a$:Knd fp$\rightarrow$ Type. ${\it da}$ $\subseteq$ ${\it da'}$ $\Rightarrow$ Valtype(${\it da'}$;$k$) $\subseteq\rho$ Valtype(${\it da}$;$k$)